Section: New Results

Concurrency-Preserving and Sound Monitoring of Multi-Threaded Component-based Systems: Theory, Algorithms, Implementation, and Evaluation

Participants : Hosein Nazarpour [Verimag] , Yliès Falcone, Saddek Bensalem [Verimag] , Marius Bozga [Verimag] .

This work addresses the monitoring of logic-independent linear-time user-provided properties in multi-threaded component-based systems. We consider intrinsically independent components that can be executed concurrently with a centralized coordination for multiparty interactions. In this context, the problem that arises is that a global state of the system is not available to the monitor. A naive solution to this problem would be to plug in a monitor which would force the system to synchronize in order to obtain the sequence of global states at run-time. Such a solution would defeat the whole purpose of having concurrent components. Instead, we reconstruct on-the-fly the global states by accumulating the partial states traversed by the system at run-time. We define transformations of components that preserve their semantics and concurrency and, at the same time, allow to monitor global-state properties. Moreover, we present RVMT-BIP, a prototype tool implementing the transformations for monitoring multi-threaded systems described in the Behavior, Interaction, Priority (BIP) framework, an expressive framework for the formal construction of heterogeneous systems. Our experiments on several multi-threaded BIP systems show that RVMT-BIP induces a cheap run-time overhead.

This work has been published in the journal Formal Aspects of Computing 2017 [4].